|
In algebraic logic, an action algebra is an algebraic structure which is both a residuated semilattice and a Kleene algebra. It adds the star or reflexive transitive closure operation of the latter to the former, while adding the left and right residuation or implication operations of the former to the latter. Unlike dynamic logic and other modal logics of programs, for which programs and propositions form two distinct sorts, action algebra combines the two into a single sort. It can be thought of as a variant of intuitionistic logic with star and with a noncommutative conjunction whose identity need not be the top element. Unlike Kleene algebras, action algebras form a variety, which furthermore is finitely axiomatizable, the crucial axiom being ''a''•(''a'' → ''a'') * ≤ ''a''. Unlike models of the equational theory of Kleene algebras (the regular expression equations), the star operation of action algebras is reflexive transitive closure in every model of the equations. ==Definition== An action algebra (''A'', ∨, 0, •, 1, ←, →, *) is an algebraic structure such that (''A'', ∨, •, 1, ←, →) forms a residuated semilattice while (''A'', ∨, 0, •, 1, *) forms a Kleene algebra. That is, it is any model of the joint theory of both classes of algebras. Now Kleene algebras are axiomatized with quasiequations, that is, implications between two or more equations, whence so are action algebras when axiomatized directly in this way. However, action algebras have the advantage that they also have an equivalent axiomatization that is purely equational.〔.〕 The language of action algebras extends in a natural way to that of action lattices, namely by the inclusion of a meet operation.〔.〕 In the following we write the inequality ''a'' ≤ ''b'' as an abbreviation for the equation ''a'' ∨ ''b'' = ''b''. This allows us to axiomatize the theory using inequalities yet still have a purely equational axiomatization when the inequalities are expanded to equalities. The equations axiomatizing action algebra are those for a residuated semilattice, together with the following equations for star. ::: 1 ∨ ''a'' *•''a'' * ∨ ''a'' ≤ ''a'' * ::: ''a'' * ≤ (''a''∨''b'') * ::: (''a'' → ''a'') * ≤ ''a'' → ''a'' The first equation can be broken out into three equations, 1 ≤ ''a'' *, ''a'' *•''a'' * ≤ ''a'' *, and ''a'' ≤ ''a'' *. These force ''a'' * to be reflexive, transitive, and greater or equal to ''a'' respectively. The second axiom asserts that star is monotone. The third axiom can be written equivalently as ''a''•(''a''→''a'') * ≤ ''a'', a form which makes its role as induction more apparent. These two axioms in conjunction with the axioms for a residuated semilattice force ''a'' * to be the least reflexive transitive element of the semilattice greater or equal to ''a''. Taking that as the definition of reflexive transitive closure of ''a'', we then have that for every element ''a'' of any action algebra, ''a'' * is the reflexive transitive closure of ''a''. The equational theory of the implication-free fragment of action algebras, those equations not containing → or ←, can be shown to coincide with the equational theory of Kleene algebras, also known as the regular expression equations. In that sense the above axioms constitute a finite axiomatization of regular expressions. Redko showed in 1967 that these equations had no finite axiomatization, for which John Horton Conway gave a shorter proof in 1971. Salomaa gave an equation schema axiomatizing this theory which Kozen subsequently reformulated as a finite axiomatization using quasiequations or implications between equations, the crucial quasiequations being those of induction: if ''x''•''a'' ≤ ''x'' then ''x''•''a'' * ≤ ''x'', and if ''a''•''x'' ≤ ''x'' then ''a'' *•''x'' ≤ ''x''. Kozen defined a Kleene algebra to be any model of this finite axiomatization. Conway showed that the equational theory of regular expressions admit models in which ''a'' * was not the reflexive transitive closure of ''a'', by giving a four-element model 0 ≤ 1 ≤ ''a'' ≤ ''a'' * in which ''a''•''a'' = ''a''. In Conway's model, ''a'' is reflexive and transitive, whence its reflexive transitive closure should be ''a''. However the regular expressions do not enforce this, allowing ''a'' * to be strictly greater than ''a''. Such anomalous behavior is not possible in an action algebra. 抄文引用元・出典: フリー百科事典『 ウィキペディア（Wikipedia）』 ■ウィキペディアで「Action algebra」の詳細全文を読む スポンサード リンク
|